(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(f, a(f, a(g, a(g, x)))) → a(g, a(g, a(g, a(f, a(f, a(f, x))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, z0)))) → c(A(g, a(g, a(g, a(f, a(f, a(f, z0)))))), A(g, a(g, a(f, a(f, a(f, z0))))), A(g, a(f, a(f, a(f, z0)))), A(f, a(f, a(f, z0))), A(f, a(f, z0)), A(f, z0))
S tuples:
A(f, a(f, a(g, a(g, z0)))) → c(A(g, a(g, a(g, a(f, a(f, a(f, z0)))))), A(g, a(g, a(f, a(f, a(f, z0))))), A(g, a(f, a(f, a(f, z0)))), A(f, a(f, a(f, z0))), A(f, a(f, z0)), A(f, z0))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
f,
a(
f,
a(
g,
a(
g,
z0)))) →
c(
A(
g,
a(
g,
a(
g,
a(
f,
a(
f,
a(
f,
z0)))))),
A(
g,
a(
g,
a(
f,
a(
f,
a(
f,
z0))))),
A(
g,
a(
f,
a(
f,
a(
f,
z0)))),
A(
f,
a(
f,
a(
f,
z0))),
A(
f,
a(
f,
z0)),
A(
f,
z0)) by
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))), A(f, a(g, a(g, z0))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
A(f, a(f, a(g, a(g, x0)))) → c
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))), A(f, a(g, a(g, z0))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
A(f, a(f, a(g, a(g, x0)))) → c
S tuples:
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))), A(f, a(g, a(g, z0))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
A(f, a(f, a(g, a(g, x0)))) → c
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
A(f, a(f, a(g, a(g, x0)))) → c
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))), A(f, a(g, a(g, z0))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
S tuples:
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))), A(f, a(g, a(g, z0))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
f,
a(
f,
a(
g,
a(
g,
a(
g,
a(
g,
z0)))))) →
c(
A(
g,
a(
g,
a(
g,
a(
f,
a(
g,
a(
g,
a(
g,
a(
f,
a(
f,
a(
f,
z0)))))))))),
A(
g,
a(
g,
a(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0))))))),
A(
g,
a(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0)))))),
A(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0))))),
A(
f,
a(
f,
a(
g,
a(
g,
z0)))),
A(
f,
a(
g,
a(
g,
z0)))) by
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
S tuples:
A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, z0))))))), A(f, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(f, a(f, a(g, a(g, z0))))), A(f, a(f, a(g, a(g, z0)))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
f,
a(
f,
a(
g,
a(
g,
a(
f,
a(
g,
a(
g,
z0))))))) →
c(
A(
g,
a(
g,
a(
g,
a(
f,
a(
f,
a(
g,
a(
g,
a(
g,
a(
f,
a(
f,
a(
f,
z0))))))))))),
A(
g,
a(
g,
a(
f,
a(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0)))))))),
A(
g,
a(
f,
a(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0))))))),
A(
f,
a(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0)))))),
A(
f,
a(
f,
a(
f,
a(
g,
a(
g,
z0))))),
A(
f,
a(
f,
a(
g,
a(
g,
z0))))) by
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
S tuples:
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c, c
(11) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0)))))) by A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
S tuples:
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c, c
(13) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0))))))) by A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
S tuples:
A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c, c
(15) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)
Used rewriting to replace A(f, a(f, a(g, a(g, a(g, a(g, x0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, x0))))))), A(g, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0)))))) by A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))
S tuples:
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c, c
(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
A(f, a(f, a(g, a(g, a(g, a(g, z0)))))) → c(A(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))), A(g, a(f, a(f, a(f, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, a(g, a(g, z0)))) → a(g, a(g, a(g, a(f, a(f, a(f, z0))))))
Tuples:
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
S tuples:
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(g, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(f, a(f, a(f, x0))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))), A(f, a(f, a(g, a(g, x0)))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))) → c(A(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))
A(f, a(f, a(g, a(g, a(f, a(g, a(g, x0))))))) → c(A(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, x0)))))))), A(g, a(f, a(f, a(f, a(f, a(g, a(g, x0))))))), A(f, a(f, a(f, a(f, a(g, a(g, x0)))))), A(f, a(f, a(f, a(g, a(g, x0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(g, a(g, z0)))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0)))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(g, a(g, z0)))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(g, a(g, z0))))))))), A(f, a(f, a(g, a(g, a(g, a(g, z0)))))), A(f, a(g, a(g, a(g, a(g, z0))))))
A(f, a(f, a(g, a(g, a(g, a(g, a(f, a(g, a(g, z0))))))))) → c(A(g, a(g, a(g, a(f, a(g, a(g, a(g, a(f, a(f, a(g, a(g, a(g, a(f, a(f, a(f, z0))))))))))))))), A(g, a(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0)))))))))), A(g, a(f, a(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))))), A(f, a(g, a(g, a(g, a(f, a(f, a(f, a(f, a(g, a(g, z0)))))))))), A(f, a(f, a(g, a(g, a(f, a(g, a(g, z0))))))), A(f, a(g, a(g, a(f, a(g, a(g, z0)))))))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c
(19) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
f0() → 0
g0() → 0
a0(0, 0) → 1
(20) BOUNDS(O(1), O(n^1))